T:Type, i:, l:T List, f:(TopTTop), y:Top.
i<||l||
 (list_accum(x,a.f(x,a);y;l)
 (~
 (list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;firstn(i;l));nth_tl(i;l))) 

latex

Definitions	True, T, as @ bs, {T}, SQType(T), nth_tl(n;as), l[i], ||as||, Prop, x(s1,s2), list_accum(x,a.f(x;a);y;l), firstn(n;as), i<j, ij, t  T, , x:A. B(x), P  Q, ij, Top, False, A, AB
Lemmas	ge wf, nat properties, nat wf, top wf, length wf1, nth tl decomp, le wf, firstn wf, select wf, firstn decomp